Nuprl Definition : normal-ds
0,22
postcript
pdf
Normal(
ds
) ==
x
dom(
ds
).
A
=
ds
(
x
)
Normal(
A
)
latex
clarification:
normal-ds{i:l}(
ds
) == fpf-all(Id; IdDeq;
ds
;
x
,
A
.normal-type{i:l}(
A
))
latex
Definitions
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
Id
,
IdDeq
,
Normal(
T
)
FDL editor aliases
normal-ds
origin
x
dom(ds). A=ds(x) 
Normal(A)
xdom(ds). A=ds(x) Normal(A)
xdom(f). v=f(x) P(x;v)